| Definitions | d-world(D;v;sched;dec), isnull(a), kind(a), s(i;t).x, a(i;t), m(i;t), 1of(t), 2of(t), P & Q, P   Q, t  T, outr(x), next-world-state(D;i;s;k;v), doact(k;v), Prop,  T, True,   x. t(x),  x:A. B(x), val(a), M.ef(k,x,s,v,w), M.ef(k,x,s,v)?w, f(x)?z, z != f(x) P(a;z), M.ds(x), true,  b, if b t else f fi, M.da(a), withlnk(l;mss), mapfilter(f;P;L), a = b, false, Top, S  T, filter(P;l), reduce(f;k;as), Y, mtag(m),  x:A. B(x), SQType(T), {T}, P  Q,  A, a in dom(M.pre), M.state, State(ds), A & B, isl(x), stutter-state(s), null, A B, False, unsolvable M.pre(a,s), w.M, Msg, vartype(i;x), Action(i), valtype(i;a), i=j, w.TA, w.T, Action(dec), d-world-state(D;i), x(s), MsgA, Valtype(da;k), Feasible(D), Unit,  , P  Q, Dec(P), Msg(M), M.rframe(k reads x), (s1  s2 mod x), M.dout(l,tg), M.init(x,v),  ,  , locl(a) |
| Lemmas | d-world-state wf, assert wf, islocal wf, ma-pre wf, d-m wf, actof wf, ma-da wf, locl wf, d-decl wf, pi1 wf, Knd wf, ma-st wf, fpf-ap wf, d-decl-subtype, IdLnk wf, subtype rel self, fpf-cap wf, top wf, ma-ef wf, member wf, d-decl-subtype2, filter filter reduce, ma-msg wf, eqof wf, idlnk-deq wf, mlnk wf d, eq id wf, lsrc wf, ma-send-val wf, ma-send-send-val, bool wf, iff transitivity, eqtt to assert, assert-eq-id, fpf-cap-void-subtype, Kind-deq wf, rcv wf, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, ma-send wf, w-withlnk wf ma, ifthenelse wf, ma-dout wf, squash wf, true wf, ma-ds wf, decidable assert, ma-send-val-nil, Msg wf, decidable ma-has-pre, d-comp-step2, action wf, false wf, isl wf, unit wf, bool cases, bool sq, id-deq wf, msga wf, Id wf, ma-state wf, fpf-dom wf, fpf-trivial-subtype-top, ma-has-pre wf, ma-npre wf, ma-decla wf2, null-action wf, eq int wf, assert of eq int, nat wf, better-d-comp-step, CV wf, d-comp wf2, le wf, ma-init-val wf |